关键词: 形状图, 形状图逻辑, Hoare逻辑, 形状分析, 程序分析

Abstract: Analysis of pointer programs has already become a hotspot research in the field of programming languages. This paper takes an approach to the problem by doing shape analysis， which uses a shape graph to express points-to and equivalence relations among pointers in a program， and uses a shape graph logic to infer programs. The shape graph logic is an extension to Hoare logic by regarding shape graphs as assertions about pointers directly. First， this paper describes the proposed shape graph and shape graph logic. Then based on the shape graph logic， it designs a method for shape analysis on pointer programs.

Key words: shape graph, shape graph logic, Hoare logic, shape analysis, program analysis